$\forall$$i$:Id, $R$:es\_realizer\{i:l\}.
\\[0ex]($\neg$($\uparrow$Rplus?($R$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($R$)))
\\[0ex]$\Rightarrow$ (R{-}da($R$; $i$) = if eq\_id(R{-}loc($R$); $i$) then Rda($R$) else fpf{-}empty fi  $\in$ fpf(Knd; $x$.Type))